Nuprl Lemma : local_or_rcv
0,22
postcript
pdf
k
:Knd. islocal(
k
)
isrcv(
k
)
latex
Definitions
Id
,
,
isl(
x
)
,
if
b
t
else
f
fi
,
b
,
IdLnk
,
t
T
,
b
,
P
Q
,
x
:
A
.
B
(
x
)
,
isrcv(
k
)
,
islocal(
k
)
,
Knd
,
,
true
,
false
,
True
,
False
,
{
T
}
Lemmas
false
wf
,
IdLnk
wf
,
Id
wf
origin
k:Knd. islocal(k) 
isrcv(k) k:Knd. islocal(k) isrcv(k) 
t else f fi
b
T
b Qx:A. B(x)